\begin{tabbing}
${\it es}$ $\equiv$ ${\it es'}$ mod ${\it es}$,$e$.$P$(${\it es}$;$e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=\{$e$:E$\mid$ $P$(${\it es}$;$e$)\}  $\equiv$ \{$e$:E$\mid$ $P$(${\it es'}$;$e$)\} \+
\\[0ex]\& ($\forall$$e$:\{$e$:E$\mid$ $P$(${\it es}$;$e$)\} . kind($e$) = kind($e$) \& loc($e$) = loc($e$))
\\[0ex]\& (\=$\forall$$e_{1}$, $e_{2}$:\{$e$:E$\mid$ $P$(${\it es}$;$e$)\} .\+
\\[0ex](($e_{1}$ $<$ $e_{2}$) $\Leftarrow\!\Rightarrow$ ($e_{1}$ $<$ $e_{2}$)) \& (val($e_{1}$) $\equiv$ val($e_{2}$) $\Leftarrow\!\Rightarrow$ val($e_{1}$) $\equiv$ val($e_{2}$)))
\-\-
\end{tabbing}